Nuprl Lemma : atom-free-level-subtype
0,22
postcript
pdf
T
:Type{i},
x
:AtomFree(Type{i};
T
).
x
AtomFree(Type{i'};
T
)
latex
Definitions
x
:
A
B
(
x
)
,
AtomFree(
T
;
x
)
,
x
:
A
.
B
(
x
)
,
t
T
,
Type
Lemmas
atom-free
wf
origin
T:Type{i}, x:AtomFree(Type{i};T). x 
AtomFree(Type{i'};T) T:Type{i}, x:AtomFree(Type{i};T). x AtomFree(Type{i'};T) 
B(x)x:A. B(x) T